/**
 * 
 * move the clauses from input to output if the clause is verified and if the formula is not invalid according
 * to the ranking given in formularanking and clauseranking
 */
__global__ void moveWS(unsigned int *input, unsigned int* output, int* validformula, int* verifiedclause, int* formularanking, int* clauseranking, int n, int batchsize)
{
	int thid = threadIdx.x;
	int blockid = blockIdx.x;
	__shared__ int formulavalid;
	__shared__ int formulapos;
	
	//blockid est le num de formule et threadid est le num de clause
	
	if(blockid < batchsize && thid < n){
		if(thid == 0){
		    formulavalid = validformula[blockid];
		    formulapos = formularanking[blockid] - 1;
		}
		__syncthreads();
		
		if(formulavalid){
			int rankc = clauseranking[thid + blockid*n] - 1;
			if(verifiedclause[thid + blockid*n]){
	    		output[formulapos*n + rankc] = input[thid + blockid*n]; 
			}
		}
	}
	__syncthreads();
}
